COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00011 ENDMK
C⊗;


(DEFPROP ITERDEF 
 (LAMBDA NIL
  (PROG (CCL INVS IBAL IVAL IGAL)
	(RETURN
	 (LIST (QUOTE DEFPROP)
 	       OP
	       (APPEND (LIST (QUOTE THCONSE))
		       (LIST
			(APPEND (VARLIST
				 (APPEND (GET OP (QUOTE IBAS))
					 (GET OP (QUOTE INVAR))
					 (GET OP (QUOTE ISTEP))
					 (GET OP (QUOTE IG))))
				(QUOTE (FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST))))
		       (LIST
			(SETQ G
			      (CONS (CAAR (LAST (CAR (GET OP (QUOTE IG)))))
				    (APPEND (ARGLIST (CDAR (LAST (CAR (GET OP (QUOTE IG)))))) (QUOTE (R))))))
		       (LIST (QUOTE (THSETQ (THV LCTR) (THV GCTR))))
		       (COND (BTSW (CONTRLTRACE (CDR (REVERSE (CDR (REVERSE G)))))) (T NIL))
		       (COND (STAT (LIST (QUOTE (SETQ THME (ADD1 THME))))) (T NIL))
		       (LIST (LIST (QUOTE TREEPATH) OP G))
		       (COND
			((GET OP (QUOTE ASSUM))
			 (LIST
			  (LIST (QUOTE THSETQ)
				(QUOTE (THV ASSL))
				(LIST (QUOTE CONS) (LIST (QUOTE QUOTE) OP) (QUOTE (THV ASSL)))))))
		       (COND (TRACESW
			      (LIST (QUOTE (TRACEINFO1)) (LIST (QUOTE THOR) T (LIST (QUOTE TRACEINFO2) OP))))
			     (T NIL))
		       (LIST
			(LIST (QUOTE COND) (LIST (LIST (QUOTE TTYIN)) (LIST (QUOTE ADVICESYS))) (QUOTE (T T))))
		       (QUOTE
			((THSETQ (THV LWF) NIL T T) (THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
						    (THSETQ (THV WF) T)
						    (THSETQ (THV LUF) NIL T T)
						    (THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
						    (THSET (CAR (THV ANS)) NIL)))
		       (REJECTQUIK ((LAMBDA (Y) (COND ((EQ Y T) NIL) (T Y))) (GET OP (QUOTE IBAS))) NIL)
		       (CSG (SUBGOALCOND ((LAMBDA (Y) (COND ((EQ Y T) NIL) (T Y))) (GET OP (QUOTE IBAS))) NIL))
		       (QUOTE ((THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T) (THSET (CAR (THV ANS)) NIL)))
		       (COND
			((NOT (GET OP (QUOTE OA)))
			 (QUOTE ((THCOND ((THV UF) (THSETQ (THV PB) NIL T T) (THGO UP1)) (T T)))))
			(T NIL))
		       (QUOTE ((THOR T (THFAIL THEOREM))))
		       (QUOTE (REP))
		       (SETQ INVS (GENINVAR (GET OP (QUOTE INVAR)) NIL))
		       (LIST (LIST (QUOTE THSETQ) (QUOTE (THV INVAR1)) (CONS (QUOTE LIST) CCL) T T))
		       (LIST
			(LIST (QUOTE THSETQ)
			      (QUOTE (THV CTST))
			      (CONS (QUOTE LIST)
				    (CONS (LIST (QUOTE QUOTE) (CAAAR (GET OP (QUOTE ICT))))
					  (CDR (PLPRED (CAAR (GET OP (QUOTE ICT))) T))))))
		       (QUOTE ((THOR T (THFAIL THEOREM))))
		       (QUOTE ((THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)))
		       (REJECTQUIK (GET OP (QUOTE ISTEP)) NIL)
		       (CSG (SUBGOALCOND (GET OP (QUOTE ISTEP)) NIL))
		       (RESETCHNGVARS IVAL)
 		       INVS
		       (DEFUNDEF IVAL)
		       (QUOTE ((THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)))
		       (LIST (LIST (QUOTE THSETQ) (QUOTE (THV INVAR2)) (CONS (QUOTE LIST) CCL) T T))
		       (QUOTE
			((THCOND ((THASVAL (THV FT))
				  (THSETQ (THV NT)
					  (COMPCHANGES (THV INVAR1)
						       (THV INVAR2)
						       (INCRELIT (THV SASSERTLITS)
								 (REVERSE (THV ASSERTLITS))))))
				 (T
				  (THSETQ (THV FT)
					  (COMPCHANGES (THV INVAR1)
						       (THV INVAR2)
						       (INCRELIT (THV SASSERTLITS)
								 (REVERSE (THV ASSERTLITS)))))))))
		       (LIST
			(LIST (QUOTE THCOND)
			      (APPEND (LIST
				       (LIST (QUOTE AND)
					     (LIST (QUOTE NOT) (QUOTE (THASVAL (THV NT))))
					     (LIST (QUOTE AMBIG) (QUOTE (THV FT)))))
				      (RESETCHNGVARS IVAL)
				      (QUOTE ((THSET (CAR (THV ANS)) NIL) (THGO REP))))
			      (QUOTE (T T))))
		       (LIST
			(LIST (QUOTE SETQ)
			      (QUOTE GTEMP)
			      (LIST (QUOTE WHILASSEM)
				    (QUOTE (THV BP))
				    (QUOTE (THV PB))
				    (QUOTE (COND ((THASVAL (THV NT)) (THV NT)) (T (THV FT))))
				    (QUOTE (THV CTST)))))
		       (QUOTE ((THSETQ (THV PB) GTEMP T T)))
		       (COND ((GET OP (QUOTE OA)) (IASSERTUP (GET OP (QUOTE OA)))) (T (UNWINDUP)))
		       (QUOTE
			((SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
			 (THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
					    (THSETQ (THV BT) NIL T T)
					    (SETQ GANS (REMBT GANS)))
				 (T T))
			 (THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
			 (THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))))
		       (LIST
			(LIST (QUOTE THCOND)
			      (LIST (QUOTE (THV ULS))
				    (LIST (QUOTE THSETQ)
					  (QUOTE (THV ASSERTLITS))
					  (LIST (QUOTE CONS)
						(LIST (QUOTE LIST)
						      (APPEND (QUOTE (LIST))
							      (LIST
							       (LIST (QUOTE QUOTE)
								     (CAR
								      (PLPRED
								       (CAR (LAST (CAR (GET OP (QUOTE IG)))))
								       NIL))))
							      (CDR
							       (PLPRED (CAR (LAST (CAR (GET OP (QUOTE IG)))))
 								       T))
							      (QUOTE ((QUOTE R))))
						      (CONS (QUOTE LIST)
							    (UNEVALARG
							     (CDR (CAR (LAST (CAR (GET OP (QUOTE IG)))))))))
						(QUOTE (THV ASSERTLITS)))))
			      (LIST T
				    (LIST (QUOTE THSETQ)
					  (QUOTE (THV WASSERTLITS))
					  (LIST (QUOTE CONS)
						(LIST (QUOTE LIST)
						      (APPEND (QUOTE (LIST))
							      (LIST
							       (LIST (QUOTE QUOTE)
								     (CAR
								      (PLPRED
								       (CAR (LAST (CAR (GET OP (QUOTE IG)))))
								       NIL))))
							      (CDR
							       (PLPRED (CAR (LAST (CAR (GET OP (QUOTE IG)))))
 								       T))
							      (QUOTE ((QUOTE R))))
						      (CONS (QUOTE LIST)
							    (UNEVALARG
							     (CDR (CAR (LAST (CAR (GET OP (QUOTE IG)))))))))
						(QUOTE (THV WASSERTLITS)))))))
		       (QUOTE ((COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))))
	       (QUOTE THEOREM))))) 
EXPR)